A:Type, B:(AType), f:fpf(A; x.B(x)). (fpf-is-empty(f))  (f = fpf-empty) 

latex

Definitions	x:A. B(x), fpf(A; a.B(a)), x(s), P  Q, fpf-is-empty(f), fpf-empty, P  Q, P  Q, P  Q, t.1, t  T, prop{i:l}, x. t(x), False, b, (i = j), ||as||, Y, tt, if b then t else f fi , True, (x  l), x:A. B(x), , A c B, A  B, A, t.2
Lemmas	assert wf, eq int wf, length wf1, fpf wf, fpf-empty wf, assert of eq int, length zero, l member wf, false wf, it wf, unit wf, pi2 wf, pi1 wf